\documentclass[12pt,stdletter,dateno,sigleft]{newlfm}
\usepackage{url}

%% \widowpenalty=1000
%% \clubpenalty=1000


\newlfmP{Headlinewd=0pt,Footlinewd=0pt}
%\newlfmP{headermarginskip=20pt}
\newlfmP{sigsize=10pt}
%\newlfmP{dateskipafter=20pt}
\newlfmP{sigskipbefore=30pt}
\newlfmP{addrfromphone}
\newlfmP{addrfromemail}
\PhrPhone{Phone}
\PhrEmail{Email}
\namefrom{Peng Fu}
\addrfrom{%
    Department of Computer Science\\
    14 MacLean Hall\\
    Iowa City, IA 52242
}
\phonefrom{218-387-4409}
\emailfrom{peng-fu@uiowa.edu \\
  \\
           \today
}

 
\greetto{To Whom It May Concern,}
 
\closeline{Sincerely,}
 
\begin{document}
\begin{newlfm}
I am writing to apply for the advertised position. I am a graduate student at University of Iowa working on language-based verification. I am expected to complete my Ph.D. dissertation on \textit{Lambda Encoding in Type Theory} and graduate by August 1, 2014.  

During my graduate studies, I have the opportunity to be involved in the $\mathrm{TRELLYS}$ project, which seeks to design a dependently-typed programming language that supports both programming and theorem proving in the same framework. I implemented a type checker for a simple programming language called SepCore and wrote a dependently typed version of AVL tree in Iowa-Trellys.

I also did research in devising a consistent intuitionistic type theory based on
lambda encodings of data. The goal of this work
is to simplify the design of a dependently typed language by adopting lambda encoding scheme instead of working with build-in data type. This work is published at the joint conference RTA(Rewriting Techniques and Applications)-TLCA(Typed Lambda Calculi and Applications).   

Currently, I am working on implementing a system that allow user to write both programs and proofs about their programs inside the same system. The novelty of this system is that no termination restriction is imposed on the program and the strong induction principle is explicit in the proof system.

I am excited about the opportunity of working with XX. Please let me know if you
have any questions about my application. 

Thank you for your consideration. I look forward to hearing from you.
\end{newlfm}
\end{document}
